<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>IndProp: Inductively Defined Propositions</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: Logical Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">IndProp<span class="subtitle">Inductively Defined Propositions</span></h1>


<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Logic</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="var">Coq.omega.Omega</span>.<br/>
</div>

<div class="doc">
<a name="lab206"></a><h1 class="section">Inductively Defined Propositions</h1>

<div class="paragraph"> </div>

 In the <a href="Logic.html"><span class="inlineref">Logic</span></a> chapter, we looked at several ways of writing
    propositions, including conjunction, disjunction, and existential
    quantification.  In this chapter, we bring yet another new tool
    into the mix: <i>inductive definitions</i>. 
<div class="paragraph"> </div>

 In past chapters, we have seen two ways of stating that a number
    <span class="inlinecode"><span class="id" type="var">n</span></span> is even: We can say

<div class="paragraph"> </div>

      (1) <span class="inlinecode"><span class="id" type="var">evenb</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>, or

<div class="paragraph"> </div>

      (2) <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">k</span>,</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span>.

<div class="paragraph"> </div>

    Yet another possibility is to say that <span class="inlinecode"><span class="id" type="var">n</span></span> is even if we can
    establish its evenness from the following rules:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Rule <span class="inlinecode"><span class="id" type="var">ev_0</span></span>: The number <span class="inlinecode">0</span> is even.

</li>
<li> Rule <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>: If <span class="inlinecode"><span class="id" type="var">n</span></span> is even, then <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> is even. 
</li>
</ul>

<div class="paragraph"> </div>

 To illustrate how this new definition of evenness works,
    let's imagine using it to show that <span class="inlinecode">4</span> is even. By rule <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>,
    it suffices to show that <span class="inlinecode">2</span> is even. This, in turn, is again
    guaranteed by rule <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>, as long as we can show that <span class="inlinecode">0</span> is
    even. But this last fact follows directly from the <span class="inlinecode"><span class="id" type="var">ev_0</span></span> rule. 
<div class="paragraph"> </div>

 We will see many definitions like this one during the rest
    of the course.  For purposes of informal discussions, it is
    helpful to have a lightweight notation that makes them easy to
    read and write.  <i>Inference rules</i> are one such notation: 
<div class="paragraph"> </div>

<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ev_0) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;0</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;n</td>
  <td class="infrulenamecol" rowspan="3">
    (ev_SS) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;(S&nbsp;(S&nbsp;n))</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 Each of the textual rules above is reformatted here as an
    inference rule; the intended reading is that, if the <i>premises</i>
    above the line all hold, then the <i>conclusion</i> below the line
    follows.  For example, the rule <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> says that, if <span class="inlinecode"><span class="id" type="var">n</span></span>
    satisfies <span class="inlinecode"><span class="id" type="var">even</span></span>, then <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> also does.  If a rule has no
    premises above the line, then its conclusion holds
    unconditionally.

<div class="paragraph"> </div>

    We can represent a proof using these rules by combining rule
    applications into a <i>proof tree</i>. Here's how we might transcribe
    the above proof that <span class="inlinecode">4</span> is even: 
<div class="paragraph"> </div>


<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;&nbsp;(<span class="id" type="var">ev_0</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;(<span class="id" type="var">ev_SS</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;2<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;(<span class="id" type="var">ev_SS</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;4
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 (Why call this a "tree" (rather than a "stack", for example)?
    Because, in general, inference rules can have multiple premises.
    We will see examples of this shortly. 
<div class="paragraph"> </div>

<a name="lab207"></a><h2 class="section">Inductive Definition of Evenness</h2>

<div class="paragraph"> </div>

 Putting all of this together, we can translate the definition of
    evenness into a formal Coq definition using an <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span>
    declaration, where each constructor corresponds to an inference
    rule: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">even</span> : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ev_0</span> : <span class="id" type="var">even</span> 0<br/>
| <span class="id" type="var">ev_SS</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">H</span> : <span class="id" type="var">even</span> <span class="id" type="var">n</span>) : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
</div>

<div class="doc">
This definition is different in one crucial respect from previous
    uses of <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span>: the thing we are defining is not a <span class="inlinecode"><span class="id" type="keyword">Type</span></span>,
    but rather a function from <span class="inlinecode"><span class="id" type="var">nat</span></span> to <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> &mdash; that is, a property
    of numbers.  We've already seen other inductive definitions that
    result in functions &mdash; for example, <span class="inlinecode"><span class="id" type="var">list</span></span>, whose type is <span class="inlinecode"><span class="id" type="keyword">Type</span></span> <span class="inlinecode">→</span>
    <span class="inlinecode"><span class="id" type="keyword">Type</span></span>.  What is really new here is that, because the <span class="inlinecode"><span class="id" type="var">nat</span></span>
    argument of <span class="inlinecode"><span class="id" type="var">even</span></span> appears to the <i>right</i> of the colon, it is
    allowed to take different values in the types of different
    constructors: <span class="inlinecode">0</span> in the type of <span class="inlinecode"><span class="id" type="var">ev_0</span></span> and <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> in the type
    of <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>.

<div class="paragraph"> </div>

    In contrast, the definition of <span class="inlinecode"><span class="id" type="var">list</span></span> names the <span class="inlinecode"><span class="id" type="var">X</span></span> parameter
    <i>globally</i>, to the <i>left</i> of the colon, forcing the result of
    <span class="inlinecode"><span class="id" type="var">nil</span></span> and <span class="inlinecode"><span class="id" type="var">cons</span></span> to be the same (<span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>).  Had we tried to bring
    <span class="inlinecode"><span class="id" type="var">nat</span></span> to the left in defining <span class="inlinecode"><span class="id" type="var">even</span></span>, we would have seen an
    error: 
</div>
<div class="code code-tight">

<span class="id" type="var">Fail</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">wrong_ev</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">wrong_ev_0</span> : <span class="id" type="var">wrong_ev</span> 0<br/>
| <span class="id" type="var">wrong_ev_SS</span> : <span class="id" type="var">wrong_ev</span> <span class="id" type="var">n</span> → <span class="id" type="var">wrong_ev</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;Error:&nbsp;Last&nbsp;occurrence&nbsp;of&nbsp;"<span class="inlinecode"><span class="id" type="var">wrong_ev</span></span>"&nbsp;must&nbsp;have&nbsp;"<span class="inlinecode"><span class="id" type="var">n</span></span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;as&nbsp;1st&nbsp;argument&nbsp;in&nbsp;"<span class="inlinecode"><span class="id" type="var">wrong_ev</span></span> <span class="inlinecode">0</span>".&nbsp;*)</span><br/>
</div>

<div class="doc">
In an <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> definition, an argument to the type
    constructor on the left of the colon is called a "parameter",
    whereas an argument on the right is called an "index".

<div class="paragraph"> </div>

    For example, in <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode">(<span class="id" type="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="keyword">Type</span>)</span> <span class="inlinecode">:=</span> <span class="inlinecode">...</span>, <span class="inlinecode"><span class="id" type="var">X</span></span> is a
    parameter; in <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> <span class="inlinecode">:=</span> <span class="inlinecode">...</span>, the
    unnamed <span class="inlinecode"><span class="id" type="var">nat</span></span> argument is an index. 
<div class="paragraph"> </div>

 We can think of the definition of <span class="inlinecode"><span class="id" type="var">even</span></span> as defining a Coq
    property <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>, together with primitive theorems
    <span class="inlinecode"><span class="id" type="var">ev_0</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">0</span> and <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span>,</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>))</span>. 
<div class="paragraph"> </div>

 That definition can also be written as follows...

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">even</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>&nbsp;:=<br/>
&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_0</span>&nbsp;:&nbsp;<span class="id" type="var">even</span>&nbsp;0<br/>
&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_SS</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="var">even</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)).
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 ... making explicit the type of the rule <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>. 
<div class="paragraph"> </div>

 Such "constructor theorems" have the same status as proven
    theorems.  In particular, we can use Coq's <span class="inlinecode"><span class="id" type="tactic">apply</span></span> tactic with the
    rule names to prove <span class="inlinecode"><span class="id" type="var">even</span></span> for particular numbers... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_4</span> : <span class="id" type="var">even</span> 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
... or we can use function application syntax: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_4'</span> : <span class="id" type="var">even</span> 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">ev_SS</span> 2 (<span class="id" type="var">ev_SS</span> 0 <span class="id" type="var">ev_0</span>)). <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
We can also prove theorems that have hypotheses involving <span class="inlinecode"><span class="id" type="var">even</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_plus4</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> (4 + <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">Hn</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Hn</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab208"></a><h4 class="section">Exercise: 1 star, standard (ev_double)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_double</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">double</span> <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab209"></a><h1 class="section">Using Evidence in Proofs</h1>

<div class="paragraph"> </div>

 Besides <i>constructing</i> evidence that numbers are even, we can also
    <i>reason about</i> such evidence.

<div class="paragraph"> </div>

    Introducing <span class="inlinecode"><span class="id" type="var">even</span></span> with an <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> declaration tells Coq not
    only that the constructors <span class="inlinecode"><span class="id" type="var">ev_0</span></span> and <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> are valid ways to
    build evidence that some number is even, but also that these two
    constructors are the <i>only</i> ways to build evidence that numbers
    are even (in the sense of <span class="inlinecode"><span class="id" type="var">even</span></span>). 
<div class="paragraph"> </div>

 In other words, if someone gives us evidence <span class="inlinecode"><span class="id" type="var">E</span></span> for the assertion
    <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>, then we know that <span class="inlinecode"><span class="id" type="var">E</span></span> must have one of two shapes:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">E</span></span> is <span class="inlinecode"><span class="id" type="var">ev_0</span></span> (and <span class="inlinecode"><span class="id" type="var">n</span></span> is <span class="inlinecode"><span class="id" type="var">O</span></span>), or

</li>
<li> <span class="inlinecode"><span class="id" type="var">E</span></span> is <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode"><span class="id" type="var">E'</span></span> (and <span class="inlinecode"><span class="id" type="var">n</span></span> is <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span>, where <span class="inlinecode"><span class="id" type="var">E'</span></span> is
        evidence for <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>). 
</li>
</ul>

<div class="paragraph"> </div>

 This suggests that it should be possible to analyze a
    hypothesis of the form <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> much as we do inductively defined
    data structures; in particular, it should be possible to argue by
    <i>induction</i> and <i>case analysis</i> on such evidence.  Let's look at a
    few examples to see what this means in practice. 
<div class="paragraph"> </div>

<a name="lab210"></a><h2 class="section">Inversion on Evidence</h2>

<div class="paragraph"> </div>

 Suppose we are proving some fact involving a number <span class="inlinecode"><span class="id" type="var">n</span></span>, and
    we are given <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> as a hypothesis.  We already know how to
    perform case analysis on <span class="inlinecode"><span class="id" type="var">n</span></span> using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> or <span class="inlinecode"><span class="id" type="tactic">induction</span></span>,
    generating separate subgoals for the case where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">O</span></span> and the
    case where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> for some <span class="inlinecode"><span class="id" type="var">n'</span></span>.  But for some proofs we may
    instead want to analyze the evidence that <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <i>directly</i>. As
    a tool, we can prove our characterization of evidence for
    <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>, using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_inversion</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>), <span class="id" type="var">even</span> <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">n</span> = 0) ∨ (<span style='font-size:120%;'>&exist;</span><span class="id" type="var">n'</span>, <span class="id" type="var">n</span> = <span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n'</span>) ∧ <span class="id" type="var">even</span> <span class="id" type="var">n'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;:&nbsp;even&nbsp;0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;:&nbsp;even&nbsp;(S&nbsp;(S&nbsp;n'))&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">n'</span>. <span class="id" type="tactic">split</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The following theorem can easily be proved using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> on
    evidence. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_minus2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> (<span class="id" type="var">pred</span> (<span class="id" type="var">pred</span> <span class="id" type="var">n</span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, this variation cannot easily be handled with <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
</div>

<div class="doc">
Intuitively, we know that evidence for the hypothesis cannot
    consist just of the <span class="inlinecode"><span class="id" type="var">ev_0</span></span> constructor, since <span class="inlinecode"><span class="id" type="var">O</span></span> and <span class="inlinecode"><span class="id" type="var">S</span></span> are
    different constructors of the type <span class="inlinecode"><span class="id" type="var">nat</span></span>; hence, <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> is the
    only case that applies.  Unfortunately, <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> is not smart
    enough to realize this, and it still generates two subgoals.  Even
    worse, in doing so, it keeps the final goal unchanged, failing to
    provide any useful information for completing the proof.  
</div>
<div class="code code-tight">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;We&nbsp;must&nbsp;prove&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;is&nbsp;even&nbsp;from&nbsp;no&nbsp;assumptions!&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
What happened, exactly?  Calling <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> has the effect of
    replacing all occurrences of the property argument by the values
    that correspond to each constructor.  This is enough in the case
    of <span class="inlinecode"><span class="id" type="var">ev_minus2</span></span> because that argument <span class="inlinecode"><span class="id" type="var">n</span></span> is mentioned directly
    in the final goal. However, it doesn't help in the case of
    <span class="inlinecode"><span class="id" type="var">evSS_ev</span></span> since the term that gets replaced (<span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>) is not
    mentioned anywhere. 
<div class="paragraph"> </div>

 We could patch this proof by replacing the goal <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>,
    which does not mention the replaced term <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>, by the
    equivalent goal <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">(<span class="id" type="var">pred</span></span> <span class="inlinecode">(<span class="id" type="var">pred</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>))))</span>, which does mention
    this term, after which <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> can make progress. But it is
    more straightforward to use our inversion lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_inversion</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span>.<br/>
&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H</span>.<br/>
&nbsp;- <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">n'</span> [<span class="id" type="var">Hnm</span> <span class="id" type="var">Hev</span>]]. <span class="id" type="tactic">injection</span> <span class="id" type="var">Hnm</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span> <span class="id" type="var">Heq</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heq</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Hev</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Coq provides a tactic called <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>, which does the work of
    our inversion lemma and more besides. 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic can detect (1) that the first case
    (<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>) does not apply and (2) that the <span class="inlinecode"><span class="id" type="var">n'</span></span> that appears in the
    <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> case must be the same as <span class="inlinecode"><span class="id" type="var">n</span></span>.  It has an "<span class="inlinecode"><span class="id" type="keyword">as</span></span>" variant
    similar to <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>, allowing us to assign names rather than
    have Coq choose them. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;We&nbsp;are&nbsp;in&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">E</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode"><span class="id" type="var">E'</span></span>&nbsp;case&nbsp;now.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic can apply the principle of explosion to
    "obviously contradictory" hypotheses involving inductive
    properties, something that takes a bit more work using our
    inversion lemma. For example: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">one_not_even</span> : ¬<span class="id" type="var">even</span> 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_inversion</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [ | [<span class="id" type="var">m</span> [<span class="id" type="var">Hm</span> <span class="id" type="var">_</span>]]].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">Hm</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">one_not_even'</span> : ¬<span class="id" type="var">even</span> 1.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab211"></a><h4 class="section">Exercise: 1 star, standard (inversion_practice)</h4>
 Prove the following result using <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>.  For extra practice,
    prove it using the inversion lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">SSSSev__even</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)))) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab212"></a><h4 class="section">Exercise: 1 star, standard (even5_nonsense)</h4>
 Prove the following result using <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">even5_nonsense</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> 5 → 2 + 2 = 9.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic does quite a bit of work. When
    applied to equalities, as a special case, it does the work of both
    <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> and <span class="inlinecode"><span class="id" type="tactic">injection</span></span>. In addition, it carries out the
    <span class="inlinecode"><span class="id" type="tactic">intros</span></span> and <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>s that are typically necessary in the case
    of <span class="inlinecode"><span class="id" type="tactic">injection</span></span>. It can also be applied, more generally, to analyze
    evidence for inductively defined propositions.  As examples, we'll
    use it to reprove some theorems from <span class="inlinecode"><span class="id" type="var">Tactics.v</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inversion_ex<sub>1</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>; <span class="id" type="var">m</span>] = [<span class="id" type="var">o</span>; <span class="id" type="var">o</span>] →<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inversion_ex<sub>2</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> = <span class="id" type="var">O</span> →<br/>
&nbsp;&nbsp;2 + 2 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">contra</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">contra</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here's how <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> works in general.  Suppose the name
    <span class="inlinecode"><span class="id" type="var">H</span></span> refers to an assumption <span class="inlinecode"><span class="id" type="var">P</span></span> in the current context, where <span class="inlinecode"><span class="id" type="var">P</span></span>
    has been defined by an <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> declaration.  Then, for each of
    the constructors of <span class="inlinecode"><span class="id" type="var">P</span></span>, <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> generates a subgoal in which
    <span class="inlinecode"><span class="id" type="var">H</span></span> has been replaced by the exact, specific conditions under
    which this constructor could have been used to prove <span class="inlinecode"><span class="id" type="var">P</span></span>.  Some of
    these subgoals will be self-contradictory; <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> throws
    these away.  The ones that are left represent the cases that must
    be proved to establish the original goal.  For those, <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>
    adds all equations into the proof context that must hold of the
    arguments given to <span class="inlinecode"><span class="id" type="var">P</span></span> (e.g., <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> in the proof of
    <span class="inlinecode"><span class="id" type="var">evSS_ev</span></span>). 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">ev_double</span></span> exercise above shows that our new notion of
    evenness is implied by the two earlier ones (since, by
    <span class="inlinecode"><span class="id" type="var">even_bool_prop</span></span> in chapter <a href="Logic.html"><span class="inlineref">Logic</span></a>, we already know that
    those are equivalent to each other). To show that all three
    coincide, we just need the following lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ev_even_firsttry</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
</div>

<div class="doc">
We could try to proceed by case analysis or induction on <span class="inlinecode"><span class="id" type="var">n</span></span>.  But
    since <span class="inlinecode"><span class="id" type="var">even</span></span> is mentioned in a premise, this strategy would
    probably lead to a dead end, as in the previous section.  Thus, it
    seems better to first try <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> on the evidence for <span class="inlinecode"><span class="id" type="var">even</span></span>.
    Indeed, the first case can be solved trivially. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>0. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
Unfortunately, the second case is harder.  We need to show <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span>
    <span class="inlinecode"><span class="id" type="var">k</span>,</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span>, but the only available assumption is
    <span class="inlinecode"><span class="id" type="var">E'</span></span>, which states that <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> holds.  Since this isn't
    directly useful, it seems that we are stuck and that performing
    case analysis on <span class="inlinecode"><span class="id" type="var">E</span></span> was a waste of time.

<div class="paragraph"> </div>

    If we look more closely at our second goal, however, we can see
    that something interesting happened: By performing case analysis
    on <span class="inlinecode"><span class="id" type="var">E</span></span>, we were able to reduce the original result to a similar
    one that involves a <i>different</i> piece of evidence for <span class="inlinecode"><span class="id" type="var">even</span></span>:
    namely <span class="inlinecode"><span class="id" type="var">E'</span></span>.  More formally, we can finish our proof by showing
    that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k'</span>,&nbsp;<span class="id" type="var">n'</span>&nbsp;=&nbsp;<span class="id" type="var">double</span>&nbsp;<span class="id" type="var">k'</span>,
<div class="paragraph"> </div>

</div>
    which is the same as the original statement, but with <span class="inlinecode"><span class="id" type="var">n'</span></span> instead
    of <span class="inlinecode"><span class="id" type="var">n</span></span>.  Indeed, it is not difficult to convince Coq that this
    intermediate result suffices. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">I</span> : (<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k'</span>, <span class="id" type="var">n'</span> = <span class="id" type="var">double</span> <span class="id" type="var">k'</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n'</span>) = <span class="id" type="var">double</span> <span class="id" type="var">k</span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" type="tactic">intros</span> [<span class="id" type="var">k'</span> <span class="id" type="var">Hk'</span>]. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk'</span>. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">S</span> <span class="id" type="var">k'</span>). <span class="id" type="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>. <span class="comment">(*&nbsp;reduce&nbsp;the&nbsp;original&nbsp;goal&nbsp;to&nbsp;the&nbsp;new&nbsp;one&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a name="lab213"></a><h2 class="section">Induction on Evidence</h2>

<div class="paragraph"> </div>

 If this looks familiar, it is no coincidence: We've
    encountered similar problems in the <a href="Induction.html"><span class="inlineref">Induction</span></a> chapter, when
    trying to use case analysis to prove results that required
    induction.  And once again the solution is... induction!

<div class="paragraph"> </div>

    The behavior of <span class="inlinecode"><span class="id" type="tactic">induction</span></span> on evidence is the same as its
    behavior on data: It causes Coq to generate one subgoal for each
    constructor that could have used to build that evidence, while
    providing an induction hypotheses for each recursive occurrence of
    the property in question.

<div class="paragraph"> </div>

    To prove a property of <span class="inlinecode"><span class="id" type="var">n</span></span> holds for all numbers for which <span class="inlinecode"><span class="id" type="var">even</span></span>
    <span class="inlinecode"><span class="id" type="var">n</span></span> holds, we can use induction on <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>. This requires us to
    prove two things, corresponding to the two ways in which <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    could have been constructed. If it was constructed by <span class="inlinecode"><span class="id" type="var">ev_0</span></span>, then
    <span class="inlinecode"><span class="id" type="var">n</span>=0</span>, and the property must hold of <span class="inlinecode">0</span>. If it was constructed by
    <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>, then the evidence of <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is of the form <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>
    <span class="inlinecode"><span class="id" type="var">E'</span></span>, where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> and <span class="inlinecode"><span class="id" type="var">E'</span></span> is evidence for <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>. In
    this case, the inductive hypothesis says that the property we are
    trying to prove holds for <span class="inlinecode"><span class="id" type="var">n'</span></span>. 
<div class="paragraph"> </div>

 Let's try our current lemma again: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ev_even</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">n'</span> <span class="id" type="var">E'</span> <span class="id" type="var">IH</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>0. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;with&nbsp;IH&nbsp;:&nbsp;exists&nbsp;k',&nbsp;n'&nbsp;=&nbsp;double&nbsp;k'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IH</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">k'</span> <span class="id" type="var">Hk'</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk'</span>. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">S</span> <span class="id" type="var">k'</span>). <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here, we can see that Coq produced an <span class="inlinecode"><span class="id" type="var">IH</span></span> that corresponds
    to <span class="inlinecode"><span class="id" type="var">E'</span></span>, the single recursive occurrence of <span class="inlinecode"><span class="id" type="var">even</span></span> in its own
    definition.  Since <span class="inlinecode"><span class="id" type="var">E'</span></span> mentions <span class="inlinecode"><span class="id" type="var">n'</span></span>, the induction hypothesis
    talks about <span class="inlinecode"><span class="id" type="var">n'</span></span>, as opposed to <span class="inlinecode"><span class="id" type="var">n</span></span> or some other number. 
<div class="paragraph"> </div>

 The equivalence between the second and third definitions of
    evenness now follows. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_even_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> ↔ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_even</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span> <span class="id" type="tactic">intros</span> [<span class="id" type="var">k</span> <span class="id" type="var">Hk</span>]. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_double</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
As we will see in later chapters, induction on evidence is a
    recurring technique across many areas, and in particular when
    formalizing the semantics of programming languages, where many
    properties of interest are defined inductively. 
<div class="paragraph"> </div>

 The following exercises provide simple examples of this
    technique, to help you familiarize yourself with it. 
<div class="paragraph"> </div>

<a name="lab214"></a><h4 class="section">Exercise: 2 stars, standard (ev_sum)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_sum</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> <span class="id" type="var">m</span> → <span class="id" type="var">even</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab215"></a><h4 class="section">Exercise: 4 stars, advanced, optional (even'_ev)</h4>
 In general, there may be multiple ways of defining a
    property inductively.  For example, here's a (slightly contrived)
    alternative definition for <span class="inlinecode"><span class="id" type="var">even</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">even'</span> : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">even'_0</span> : <span class="id" type="var">even'</span> 0<br/>
| <span class="id" type="var">even'_2</span> : <span class="id" type="var">even'</span> 2<br/>
| <span class="id" type="var">even'_sum</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> (<span class="id" type="var">Hn</span> : <span class="id" type="var">even'</span> <span class="id" type="var">n</span>) (<span class="id" type="var">Hm</span> : <span class="id" type="var">even'</span> <span class="id" type="var">m</span>) : <span class="id" type="var">even'</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>).<br/>
</div>

<div class="doc">
Prove that this definition is logically equivalent to the old
    one.  (You may want to look at the previous theorem when you get
    to the induction step.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">even'_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even'</span> <span class="id" type="var">n</span> ↔ <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab216"></a><h4 class="section">Exercise: 3 stars, advanced, recommended (ev_ev__ev)</h4>
 Finding the appropriate thing to do induction on is a
    bit tricky here: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_ev__ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">m</span>) → <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab217"></a><h4 class="section">Exercise: 3 stars, standard, optional (ev_plus_plus)</h4>
 This exercise just requires applying existing lemmas.  No
    induction or even case analysis is needed, though some of the
    rewriting may be tedious. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_plus_plus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">m</span>) → <span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">p</span>) → <span class="id" type="var">even</span> (<span class="id" type="var">m</span>+<span class="id" type="var">p</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab218"></a><h1 class="section">Inductive Relations</h1>

<div class="paragraph"> </div>

 A proposition parameterized by a number (such as <span class="inlinecode"><span class="id" type="var">even</span></span>)
    can be thought of as a <i>property</i> &mdash; i.e., it defines
    a subset of <span class="inlinecode"><span class="id" type="var">nat</span></span>, namely those numbers for which the proposition
    is provable.  In the same way, a two-argument proposition can be
    thought of as a <i>relation</i> &mdash; i.e., it defines a set of pairs for
    which the proposition is provable. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Playground</span>.<br/>
</div>

<div class="doc">
One useful example is the "less than or equal to" relation on
    numbers. 
<div class="paragraph"> </div>

 The following definition should be fairly intuitive.  It
    says that there are two ways to give evidence that one number is
    less than or equal to another: either observe that they are the
    same number, or give evidence that the first is less than or equal
    to the predecessor of the second. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">le</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">le_n</span> <span class="id" type="var">n</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">le_S</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> (<span class="id" type="var">H</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>) : <span class="id" type="var">le</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "m ≤ n" := (<span class="id" type="var">le</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>).<br/>
</div>

<div class="doc">
Proofs of facts about <span class="inlinecode">≤</span> using the constructors <span class="inlinecode"><span class="id" type="var">le_n</span></span> and
    <span class="inlinecode"><span class="id" type="var">le_S</span></span> follow the same patterns as proofs about properties, like
    <span class="inlinecode"><span class="id" type="var">even</span></span> above. We can <span class="inlinecode"><span class="id" type="tactic">apply</span></span> the constructors to prove <span class="inlinecode">≤</span>
    goals (e.g., to show that <span class="inlinecode">3≤3</span> or <span class="inlinecode">3≤6</span>), and we can use
    tactics like <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> to extract information from <span class="inlinecode">≤</span>
    hypotheses in the context (e.g., to prove that <span class="inlinecode">(2</span> <span class="inlinecode">≤</span> <span class="inlinecode">1)</span> <span class="inlinecode">→</span>
    <span class="inlinecode">2+2=5</span>.) 
<div class="paragraph"> </div>

 Here are some sanity checks on the definition.  (Notice that,
    although these are the same kind of simple "unit tests" as we gave
    for the testing functions we wrote in the first few lectures, we
    must construct their proofs explicitly &mdash; <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> and
    <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> don't do the job, because the proofs aren't just a
    matter of simplifying computations.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>1</sub></span> :<br/>
&nbsp;&nbsp;3 ≤ 3.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>2</sub></span> :<br/>
&nbsp;&nbsp;3 ≤ 6.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>3</sub></span> :<br/>
&nbsp;&nbsp;(2 ≤ 1) → 2 + 2 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The "strictly less than" relation <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">&lt;</span> <span class="inlinecode"><span class="id" type="var">m</span></span> can now be defined
    in terms of <span class="inlinecode"><span class="id" type="var">le</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Playground</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">lt</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span>:<span class="id" type="var">nat</span>) := <span class="id" type="var">le</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) <span class="id" type="var">m</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "m &lt; n" := (<span class="id" type="var">lt</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>).<br/>
</div>

<div class="doc">
Here are a few more simple relations on numbers: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">square_of</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">sq</span> <span class="id" type="var">n</span> : <span class="id" type="var">square_of</span> <span class="id" type="var">n</span> (<span class="id" type="var">n</span> * <span class="id" type="var">n</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">next_nat</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nn</span> <span class="id" type="var">n</span> : <span class="id" type="var">next_nat</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">next_even</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ne_1</span> <span class="id" type="var">n</span> : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) → <span class="id" type="var">next_even</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ne_2</span> <span class="id" type="var">n</span> (<span class="id" type="var">H</span> : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>))) : <span class="id" type="var">next_even</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
</div>

<div class="doc">
<a name="lab219"></a><h4 class="section">Exercise: 2 stars, standard, optional (total_relation)</h4>
 Define an inductive binary relation <span class="inlinecode"><span class="id" type="var">total_relation</span></span> that holds
    between every pair of natural numbers. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab220"></a><h4 class="section">Exercise: 2 stars, standard, optional (empty_relation)</h4>
 Define an inductive binary relation <span class="inlinecode"><span class="id" type="var">empty_relation</span></span> (on numbers)
    that never holds. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 From the definition of <span class="inlinecode"><span class="id" type="var">le</span></span>, we can sketch the behaviors of
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>, <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>, and <span class="inlinecode"><span class="id" type="tactic">induction</span></span> on a hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span>
    providing evidence of the form <span class="inlinecode"><span class="id" type="var">le</span></span> <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span>.  Doing <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    will generate two cases. In the first case, <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span>, and it
    will replace instances of <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> with <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> in the goal and context.
    In the second case, <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> for some <span class="inlinecode"><span class="id" type="var">n'</span></span> for which <span class="inlinecode"><span class="id" type="var">le</span></span> <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>
    holds, and it will replace instances of <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> with <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>. 
    Doing <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> will remove impossible cases and add generated
    equalities to the context for further use. Doing <span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    will, in the second case, add the induction hypothesis that the
    goal holds when <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> is replaced with <span class="inlinecode"><span class="id" type="var">n'</span></span>. 
<div class="paragraph"> </div>

<a name="lab221"></a><h4 class="section">Exercise: 3 stars, standard, optional (le_exercises)</h4>
 Here are a number of facts about the <span class="inlinecode">≤</span> and <span class="inlinecode">&lt;</span> relations that
    we are going to need later in the course.  The proofs make good
    practice exercises. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">le_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>, <span class="id" type="var">m</span> ≤ <span class="id" type="var">n</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">o</span> → <span class="id" type="var">m</span> ≤ <span class="id" type="var">o</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">O_le_n</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;0 ≤ <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">n_le_m__Sn_le_Sm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> → <span class="id" type="var">S</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">S</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">Sn_le_Sm__n_le_m</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">S</span> <span class="id" type="var">m</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">le_plus_l</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">b</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">a</span> ≤ <span class="id" type="var">a</span> + <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_lt</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span> &lt; <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n<sub>1</sub></span> &lt; <span class="id" type="var">m</span> ∧ <span class="id" type="var">n<sub>2</sub></span> &lt; <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">lt</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lt_S</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt; <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt; <span class="id" type="var">S</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_complete</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Hint: The next one may be easiest to prove by induction on <span class="inlinecode"><span class="id" type="var">m</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_correct</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Hint: This one can easily be proved without using <span class="inlinecode"><span class="id" type="tactic">induction</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_true_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> → <span class="id" type="var">m</span> &lt;=? <span class="id" type="var">o</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> &lt;=? <span class="id" type="var">o</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab222"></a><h4 class="section">Exercise: 2 stars, standard, optional (leb_iff)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> ↔ <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">R</span>.<br/>
</div>

<div class="doc">
<a name="lab223"></a><h4 class="section">Exercise: 3 stars, standard, recommended (R_provability)</h4>
 We can define three-place relations, four-place relations,
    etc., in just the same way as binary relations.  For example,
    consider the following three-place relation on numbers: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">R</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> : <span class="id" type="var">R</span> 0 0 0<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>) <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">o</span>)<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> <span class="id" type="var">m</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) (<span class="id" type="var">S</span> <span class="id" type="var">o</span>)<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>4</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>) (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">o</span>))) : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span><br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>5</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span>.<br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<ul class="doclist">
<li> Which of the following propositions are provable?
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">1</span> <span class="inlinecode">1</span> <span class="inlinecode">2</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">2</span> <span class="inlinecode">2</span> <span class="inlinecode">6</span>

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If we dropped constructor <span class="inlinecode"><span class="id" type="var">c<sub>5</sub></span></span> from the definition of <span class="inlinecode"><span class="id" type="var">R</span></span>,
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

<div class="paragraph"> </div>


</li>
<li> If we dropped constructor <span class="inlinecode"><span class="id" type="var">c<sub>4</sub></span></span> from the definition of <span class="inlinecode"><span class="id" type="var">R</span></span>,
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

</li>
</ul>

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_R_provability</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab224"></a><h4 class="section">Exercise: 3 stars, standard, optional (R_fact)</h4>
 The relation <span class="inlinecode"><span class="id" type="var">R</span></span> above actually encodes a familiar function.
    Figure out which function; then state and prove this equivalence
    in Coq? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fR</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">R_equiv_fR</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>, <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> ↔ <span class="id" type="var">fR</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> = <span class="id" type="var">o</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">R</span>.<br/>
</div>

<div class="doc">
<a name="lab225"></a><h4 class="section">Exercise: 2 stars, advanced (subsequence)</h4>
 A list is a <i>subsequence</i> of another list if all of the elements
    in the first list occur in the same order in the second list,
    possibly with some extra elements in between. For example,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;3]
<div class="paragraph"> </div>

</div>
    is a subsequence of each of the lists

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;1;1;2;2;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;7;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[5;6;1;9;9;2;7;3;8]
<div class="paragraph"> </div>

</div>
    but it is <i>not</i> a subsequence of any of the lists

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[5;6;2;1;7;3;8].
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

<ul class="doclist">
<li> Define an inductive proposition <span class="inlinecode"><span class="id" type="var">subseq</span></span> on <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> that
      captures what it means to be a subsequence. (Hint: You'll need
      three cases.)

<div class="paragraph"> </div>


</li>
<li> Prove <span class="inlinecode"><span class="id" type="var">subseq_refl</span></span> that subsequence is reflexive, that is,
      any list is a subsequence of itself.

<div class="paragraph"> </div>


</li>
<li> Prove <span class="inlinecode"><span class="id" type="var">subseq_app</span></span> that for any lists <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span>,
      if <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> is a subsequence of <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, then <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> is also a subsequence
      of <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> (Optional, harder) Prove <span class="inlinecode"><span class="id" type="var">subseq_trans</span></span> that subsequence is
      transitive &mdash; that is, if <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> is a subsequence of <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>
      is a subsequence of <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span>, then <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> is a subsequence of <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span>.
      Hint: choose your induction carefully! 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">subseq</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span> → <span class="id" type="var">list</span> <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_refl</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>), <span class="id" type="var">subseq</span> <span class="id" type="var">l</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_app</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> (<span class="id" type="var">l<sub>2</sub></span> ++ <span class="id" type="var">l<sub>3</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_trans</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>3</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab226"></a><h4 class="section">Exercise: 2 stars, standard, optional (R_provability2)</h4>
 Suppose we give Coq the following definition:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">R</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;:&nbsp;<span class="id" type="var">R</span>&nbsp;0&nbsp;[]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>2</sub></span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">R</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">R</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)&nbsp;(<span class="id" type="var">n</span>&nbsp;::&nbsp;<span class="id" type="var">l</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>3</sub></span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">R</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">R</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>
    Which of the following propositions are provable?

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">2</span> <span class="inlinecode">[1;0]</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">1</span> <span class="inlinecode">[1;2;1;0]</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">6</span> <span class="inlinecode">[3;2;1;0]</span>  
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab227"></a><h1 class="section">Case Study: Regular Expressions</h1>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">even</span></span> property provides a simple example for
    illustrating inductive definitions and the basic techniques for
    reasoning about them, but it is not terribly exciting &mdash; after
    all, it is equivalent to the two non-inductive definitions of
    evenness that we had already seen, and does not seem to offer any
    concrete benefit over them.

<div class="paragraph"> </div>

    To give a better sense of the power of inductive definitions, we
    now show how to use them to model a classic concept in computer
    science: <i>regular expressions</i>. 
<div class="paragraph"> </div>

 Regular expressions are a simple language for describing sets of
    strings.  Their syntax is defined as follows: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">reg_exp</span> {<span class="id" type="var">T</span> : <span class="id" type="keyword">Type</span>} : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> (<span class="id" type="var">t</span> : <span class="id" type="var">T</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> (<span class="id" type="var">r<sub>1</sub></span> <span class="id" type="var">r<sub>2</sub></span> : <span class="id" type="var">reg_exp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> (<span class="id" type="var">r<sub>1</sub></span> <span class="id" type="var">r<sub>2</sub></span> : <span class="id" type="var">reg_exp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> (<span class="id" type="var">r</span> : <span class="id" type="var">reg_exp</span>).<br/>
</div>

<div class="doc">
Note that this definition is <i>polymorphic</i>: Regular
    expressions in <span class="inlinecode"><span class="id" type="var">reg_exp</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> describe strings with characters drawn
    from <span class="inlinecode"><span class="id" type="var">T</span></span> &mdash; that is, lists of elements of <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

    (We depart slightly from standard practice in that we do not
    require the type <span class="inlinecode"><span class="id" type="var">T</span></span> to be finite.  This results in a somewhat
    different theory of regular expressions, but the difference is not
    significant for our purposes.) 
<div class="paragraph"> </div>

 We connect regular expressions and strings via the following
    rules, which define when a regular expression <i>matches</i> some
    string:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The expression <span class="inlinecode"><span class="id" type="var">EmptySet</span></span> does not match any string.

<div class="paragraph"> </div>


</li>
<li> The expression <span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> matches the empty string <span class="inlinecode">[]</span>.

<div class="paragraph"> </div>


</li>
<li> The expression <span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> matches the one-character string <span class="inlinecode">[<span class="id" type="var">x</span>]</span>.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>,
        then <span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> If at least one of <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">s</span></span>,
        then <span class="inlinecode"><span class="id" type="var">Union</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">s</span></span>.

<div class="paragraph"> </div>


</li>
<li> Finally, if we can write some string <span class="inlinecode"><span class="id" type="var">s</span></span> as the concatenation
        of a sequence of strings <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s_1</span></span> <span class="inlinecode">++</span> <span class="inlinecode">...</span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s_k</span></span>, and the
        expression <span class="inlinecode"><span class="id" type="var">re</span></span> matches each one of the strings <span class="inlinecode"><span class="id" type="var">s_i</span></span>,
        then <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> matches <span class="inlinecode"><span class="id" type="var">s</span></span>.

<div class="paragraph"> </div>

        As a special case, the sequence of strings may be empty, so
        <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> always matches the empty string <span class="inlinecode">[]</span> no matter what
        <span class="inlinecode"><span class="id" type="var">re</span></span> is. 
</li>
</ul>

<div class="paragraph"> </div>

 We can easily translate this informal definition into an
    <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> one as follows: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">exp_match</span> {<span class="id" type="var">T</span>} : <span class="id" type="var">list</span> <span class="id" type="var">T</span> → <span class="id" type="var">reg_exp</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">MEmpty</span> : <span class="id" type="var">exp_match</span> [] <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">MChar</span> <span class="id" type="var">x</span> : <span class="id" type="var">exp_match</span> [<span class="id" type="var">x</span>] (<span class="id" type="var">Char</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MApp</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> (<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MUnionL</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> (<span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MUnionR</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> (<span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MStar0</span> <span class="id" type="var">re</span> : <span class="id" type="var">exp_match</span> [] (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MStarApp</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>)) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> (<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
Again, for readability, we can also display this definition using
    inference-rule notation.  At the same time, let's introduce a more
    readable infix notation. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "s =~ re" := (<span class="id" type="var">exp_match</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80).<br/>
</div>

<div class="doc">
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MEmpty) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[]&nbsp;=~&nbsp;EmptyStr</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MChar) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[x]&nbsp;=~&nbsp;Char&nbsp;x</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;re<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;++&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;App&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MUnionL) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;Union&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>2</sub>&nbsp;=~&nbsp;re<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MUnionR) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>2</sub>&nbsp;=~&nbsp;Union&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MStar0) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[]&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re&nbsp;&nbsp;&nbsp;&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td class="infrulenamecol" rowspan="3">
    (MStarApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;++&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 Notice that these rules are not <i>quite</i> the same as the
    informal ones that we gave at the beginning of the section.
    First, we don't need to include a rule explicitly stating that no
    string matches <span class="inlinecode"><span class="id" type="var">EmptySet</span></span>; we just don't happen to include any
    rule that would have the effect of some string matching
    <span class="inlinecode"><span class="id" type="var">EmptySet</span></span>.  (Indeed, the syntax of inductive definitions doesn't
    even <i>allow</i> us to give such a "negative rule.")

<div class="paragraph"> </div>

    Second, the informal rules for <span class="inlinecode"><span class="id" type="var">Union</span></span> and <span class="inlinecode"><span class="id" type="var">Star</span></span> correspond
    to two constructors each: <span class="inlinecode"><span class="id" type="var">MUnionL</span></span> / <span class="inlinecode"><span class="id" type="var">MUnionR</span></span>, and <span class="inlinecode"><span class="id" type="var">MStar0</span></span> /
    <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>.  The result is logically equivalent to the original
    rules but more convenient to use in Coq, since the recursive
    occurrences of <span class="inlinecode"><span class="id" type="var">exp_match</span></span> are given as direct arguments to the
    constructors, making it easier to perform induction on evidence.
    (The <span class="inlinecode"><span class="id" type="var">exp_match_ex<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">exp_match_ex<sub>2</sub></span></span> exercises below ask you
    to prove that the constructors given in the inductive declaration
    and the ones that would arise from a more literal transcription of
    the informal rules are indeed equivalent.)

<div class="paragraph"> </div>

    Let's illustrate these rules with a few examples. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>1</sub></span> : [1] =~ <span class="id" type="var">Char</span> 1.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>2</sub></span> : [1; 2] =~ <span class="id" type="var">App</span> (<span class="id" type="var">Char</span> 1) (<span class="id" type="var">Char</span> 2).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [1] <span class="id" type="var">_</span> [2]).<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
(Notice how the last example applies <span class="inlinecode"><span class="id" type="var">MApp</span></span> to the strings
    <span class="inlinecode">[1]</span> and <span class="inlinecode">[2]</span> directly.  Since the goal mentions <span class="inlinecode">[1;</span> <span class="inlinecode">2]</span>
    instead of <span class="inlinecode">[1]</span> <span class="inlinecode">++</span> <span class="inlinecode">[2]</span>, Coq wouldn't be able to figure out how to
    split the string on its own.)

<div class="paragraph"> </div>

    Using <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>, we can also show that certain strings do <i>not</i>
    match a regular expression: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>3</sub></span> : ¬([1; 2] =~ <span class="id" type="var">Char</span> 1).<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
We can define helper functions for writing down regular
    expressions. The <span class="inlinecode"><span class="id" type="var">reg_exp_of_list</span></span> function constructs a regular
    expression that matches exactly the list that it receives as an
    argument: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">reg_exp_of_list</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span> :: <span class="id" type="var">l'</span> ⇒ <span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">x</span>) (<span class="id" type="var">reg_exp_of_list</span> <span class="id" type="var">l'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>4</sub></span> : [1; 2; 3] =~ <span class="id" type="var">reg_exp_of_list</span> [1; 2; 3].<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [1]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [2]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [3]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MEmpty</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
We can also prove general facts about <span class="inlinecode"><span class="id" type="var">exp_match</span></span>.  For instance,
    the following lemma shows that every string <span class="inlinecode"><span class="id" type="var">s</span></span> that matches <span class="inlinecode"><span class="id" type="var">re</span></span>
    also matches <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar1</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> <span class="id" type="var">s</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) ,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- (<span class="id" type="var">app_nil_r</span> <span class="id" type="var">_</span> <span class="id" type="var">s</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MStarApp</span> <span class="id" type="var">s</span> [] <span class="id" type="var">re</span>).<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MStar0</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
(Note the use of <span class="inlinecode"><span class="id" type="var">app_nil_r</span></span> to change the goal of the theorem to
    exactly the same shape expected by <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>.) 
<div class="paragraph"> </div>

<a name="lab228"></a><h4 class="section">Exercise: 3 stars, standard (exp_match_ex<sub>1</sub>)</h4>
 The following lemmas show that the informal matching rules given
    at the beginning of the chapter can be obtained from the formal
    inductive definition. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_is_empty</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;¬(<span class="id" type="var">s</span> =~ <span class="id" type="var">EmptySet</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MUnion'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span> ∨ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
The next lemma is stated in terms of the <span class="inlinecode"><span class="id" type="var">fold</span></span> function from the
    <a href="Poly.html"><span class="inlineref">Poly</span></a> chapter: If <span class="inlinecode"><span class="id" type="var">ss</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode">(<span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">T</span>)</span> represents a sequence of
    strings <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span>,</span> <span class="inlinecode">...,</span> <span class="inlinecode"><span class="id" type="var">sn</span></span>, then <span class="inlinecode"><span class="id" type="var">fold</span></span> <span class="inlinecode"><span class="id" type="var">app</span></span> <span class="inlinecode"><span class="id" type="var">ss</span></span> <span class="inlinecode">[]</span> is the result of
    concatenating them all together. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">ss</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">T</span>)) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">s</span>, <span class="id" type="var">In</span> <span class="id" type="var">s</span> <span class="id" type="var">ss</span> → <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> <span class="id" type="var">app</span> <span class="id" type="var">ss</span> [] =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab229"></a><h4 class="section">Exercise: 4 stars, standard, optional (reg_exp_of_list_spec)</h4>
 Prove that <span class="inlinecode"><span class="id" type="var">reg_exp_of_list</span></span> satisfies the following
    specification: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">reg_exp_of_list_spec</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">reg_exp_of_list</span> <span class="id" type="var">s<sub>2</sub></span> ↔ <span class="id" type="var">s<sub>1</sub></span> = <span class="id" type="var">s<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Since the definition of <span class="inlinecode"><span class="id" type="var">exp_match</span></span> has a recursive
    structure, we might expect that proofs involving regular
    expressions will often require induction on evidence. 
<div class="paragraph"> </div>

 For example, suppose that we wanted to prove the following
    intuitive result: If a regular expression <span class="inlinecode"><span class="id" type="var">re</span></span> matches some string
    <span class="inlinecode"><span class="id" type="var">s</span></span>, then all elements of <span class="inlinecode"><span class="id" type="var">s</span></span> must occur as character literals
    somewhere in <span class="inlinecode"><span class="id" type="var">re</span></span>.

<div class="paragraph"> </div>

    To state this theorem, we first define a function <span class="inlinecode"><span class="id" type="var">re_chars</span></span> that
    lists all characters that occur in a regular expression: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">re_chars</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>) : <span class="id" type="var">list</span> <span class="id" type="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">re</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span> ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span> ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> <span class="id" type="var">x</span> ⇒ [<span class="id" type="var">x</span>]<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>1</sub></span> ++ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>1</sub></span> ++ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> <span class="id" type="var">re</span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;/HIDEFROMHTML&nbsp;*)</span><br/>
</div>

<div class="doc">
We can then phrase our theorem as follows: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">in_re_match</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> (<span class="id" type="var">re_chars</span> <span class="id" type="var">re</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span> <span class="id" type="var">x</span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hmatch</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [| <span class="id" type="var">x'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span> | <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">re</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span> <span class="id" type="keyword">in</span> *.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Hin</span> | <span class="id" type="var">Hin</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>1</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>2</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>2</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionL&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH</span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionR&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH</span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStar0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span>.<br/>
</div>

<div class="doc">
Something interesting happens in the <span class="inlinecode"><span class="id" type="var">MStarApp</span></span> case.  We obtain
    <i>two</i> induction hypotheses: One that applies when <span class="inlinecode"><span class="id" type="var">x</span></span> occurs in
    <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> (which matches <span class="inlinecode"><span class="id" type="var">re</span></span>), and a second one that applies when <span class="inlinecode"><span class="id" type="var">x</span></span>
    occurs in <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> (which matches <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>).  This is a good
    illustration of why we need induction on evidence for <span class="inlinecode"><span class="id" type="var">exp_match</span></span>,
    rather than induction on the regular expression <span class="inlinecode"><span class="id" type="var">re</span></span>: The latter
    would only provide an induction hypothesis for strings that match
    <span class="inlinecode"><span class="id" type="var">re</span></span>, which would not allow us to reason about the case <span class="inlinecode"><span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>
    <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStarApp&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Hin</span> | <span class="id" type="var">Hin</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>1</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>2</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>2</sub></span> <span class="id" type="var">Hin</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab230"></a><h4 class="section">Exercise: 4 stars, standard (re_not_empty)</h4>
 Write a recursive function <span class="inlinecode"><span class="id" type="var">re_not_empty</span></span> that tests whether a
    regular expression matches some string. Prove that your function
    is correct. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">re_not_empty</span> {<span class="id" type="var">T</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">re_not_empty_correct</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s</span>, <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) ↔ <span class="id" type="var">re_not_empty</span> <span class="id" type="var">re</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab231"></a><h2 class="section">The <span class="inlinecode"><span class="id" type="var">remember</span></span> Tactic</h2>

<div class="paragraph"> </div>

 One potentially confusing feature of the <span class="inlinecode"><span class="id" type="tactic">induction</span></span> tactic is
    that it will let you try to perform an induction over a term that
    isn't sufficiently general.  The effect of this is to lose
    information (much as <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> without an <span class="inlinecode"><span class="id" type="var">eqn</span>:</span> clause can do),
    and leave you unable to complete the proof.  Here's an example: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
</div>

<div class="doc">
Just doing an <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> on <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> won't get us very far in
    the recursive cases. (Try it!). So we need induction (on
    evidence!). Here is a naive first attempt: 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [|<span class="id" type="var">x'</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span>|<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">re''</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re''</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
</div>

<div class="doc">
But now, although we get seven cases (as we would expect from the
    definition of <span class="inlinecode"><span class="id" type="var">exp_match</span></span>), we have lost a very important bit of
    information from <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span>: the fact that <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> matched something of the
    form <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>.  This means that we have to give proofs for <i>all</i>
    seven constructors of this definition, even though all but two of
    them (<span class="inlinecode"><span class="id" type="var">MStar0</span></span> and <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>) are contradictory.  We can still
    get the proof to go through for a few constructors, such as
    <span class="inlinecode"><span class="id" type="var">MEmpty</span></span>... 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
</div>

<div class="doc">
... but most cases get stuck.  For <span class="inlinecode"><span class="id" type="var">MChar</span></span>, for instance, we
    must show that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span>&nbsp;=~&nbsp;<span class="id" type="var">Char</span>&nbsp;<span class="id" type="var">x'</span>&nbsp;→&nbsp;<span class="id" type="var">x'</span>&nbsp;::&nbsp;<span class="id" type="var">s<sub>2</sub></span>&nbsp;=~&nbsp;<span class="id" type="var">Char</span>&nbsp;<span class="id" type="var">x'</span>,
<div class="paragraph"> </div>

</div>
    which is clearly impossible. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar.&nbsp;Stuck...&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The problem is that <span class="inlinecode"><span class="id" type="tactic">induction</span></span> over a Prop hypothesis only works
    properly with hypotheses that are completely general, i.e., ones
    in which all the arguments are variables, as opposed to more
    complex expressions, such as <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>.

<div class="paragraph"> </div>

    (In this respect, <span class="inlinecode"><span class="id" type="tactic">induction</span></span> on evidence behaves more like
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>-without-<span class="inlinecode"><span class="id" type="var">eqn</span>:</span> than like <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>.)

<div class="paragraph"> </div>

    An awkward way to solve this problem is "manually generalizing" 
    over the problematic expressions by adding explicit equality 
    hypotheses to the lemma: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> <span class="id" type="var">re'</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">re'</span> = <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
</div>

<div class="doc">
We can now proceed by performing induction over evidence directly,
    because the argument to the first hypothesis is sufficiently
    general, which means that we can discharge most cases by inverting
    the <span class="inlinecode"><span class="id" type="var">re'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> equality in the context.

<div class="paragraph"> </div>

    This idiom is so common that Coq provides a tactic to
    automatically generate such equations for us, avoiding thus the
    need for changing the statements of our theorems. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" type="var">remember</span></span> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> causes Coq to (1) replace all
    occurrences of the expression <span class="inlinecode"><span class="id" type="var">e</span></span> by the variable <span class="inlinecode"><span class="id" type="var">x</span></span>, and (2) add
    an equation <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> to the context.  Here's how we can use it to
    show the above result: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">re'</span>.<br/>
</div>

<div class="doc">
We now have <span class="inlinecode"><span class="id" type="var">Heqre'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">re'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">s<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [|<span class="id" type="var">x'</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span>|<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">re''</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re''</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="var">Heqre'</span></span> is contradictory in most cases, allowing us to
    conclude immediately. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span>  <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar&nbsp;*)</span>   <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MApp&nbsp;*)</span>    <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionL&nbsp;*)</span> <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionR&nbsp;*)</span> <span class="id" type="tactic">discriminate</span>.<br/>
</div>

<div class="doc">
The interesting cases are those that correspond to <span class="inlinecode"><span class="id" type="var">Star</span></span>.  Note
    that the induction hypothesis <span class="inlinecode"><span class="id" type="var">IH<sub>2</sub></span></span> on the <span class="inlinecode"><span class="id" type="var">MStarApp</span></span> case
    mentions an additional premise <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re''</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re'</span></span>, which
    results from the equality generated by <span class="inlinecode"><span class="id" type="var">remember</span></span>. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStar0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">Heqre'</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">Heqre''</span> <span class="id" type="var">s</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStarApp&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">Heqre'</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">app_assoc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MStarApp</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">Hmatch1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">IH<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab232"></a><h4 class="section">Exercise: 4 stars, standard, optional (exp_match_ex<sub>2</sub>)</h4>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">MStar''</span></span> lemma below (combined with its converse, the
    <span class="inlinecode"><span class="id" type="var">MStar'</span></span> exercise above), shows that our definition of <span class="inlinecode"><span class="id" type="var">exp_match</span></span>
    for <span class="inlinecode"><span class="id" type="var">Star</span></span> is equivalent to the informal one given previously. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar''</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ss</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">fold</span> <span class="id" type="var">app</span> <span class="id" type="var">ss</span> []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;∧ <span style='font-size:120%;'>&forall;</span><span class="id" type="var">s'</span>, <span class="id" type="var">In</span> <span class="id" type="var">s'</span> <span class="id" type="var">ss</span> → <span class="id" type="var">s'</span> =~ <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab233"></a><h4 class="section">Exercise: 5 stars, advanced (pumping)</h4>
 One of the first really interesting theorems in the theory of
    regular expressions is the so-called <i>pumping lemma</i>, which
    states, informally, that any sufficiently long string <span class="inlinecode"><span class="id" type="var">s</span></span> matching
    a regular expression <span class="inlinecode"><span class="id" type="var">re</span></span> can be "pumped" by repeating some middle
    section of <span class="inlinecode"><span class="id" type="var">s</span></span> an arbitrary number of times to produce a new
    string also matching <span class="inlinecode"><span class="id" type="var">re</span></span>.

<div class="paragraph"> </div>

    To begin, we need to define "sufficiently long."  Since we are
    working in a constructive logic, we actually need to be able to
    calculate, for each regular expression <span class="inlinecode"><span class="id" type="var">re</span></span>, the minimum length
    for strings <span class="inlinecode"><span class="id" type="var">s</span></span> to guarantee "pumpability." 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Pumping</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pumping_constant</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">re</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span> ⇒ 0<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span> ⇒ 1<br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> <span class="id" type="var">_</span> ⇒ 2<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>1</sub></span> + <span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>1</sub></span> + <span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> <span class="id" type="var">_</span> ⇒ 1<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
Next, it is useful to define an auxiliary function that repeats a
    string (appends it to itself) some number of times. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">napp</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) : <span class="id" type="var">list</span> <span class="id" type="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">n</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">n'</span> ⇒ <span class="id" type="var">l</span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">n'</span> <span class="id" type="var">l</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">napp_plus</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">napp</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>) <span class="id" type="var">l</span> = <span class="id" type="var">napp</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">m</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">l</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">n</span> <span class="id" type="var">IHn</span>].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHn</span>, <span class="id" type="var">app_assoc</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Now, the pumping lemma itself says that, if <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re</span></span> and if the
    length of <span class="inlinecode"><span class="id" type="var">s</span></span> is at least the pumping constant of <span class="inlinecode"><span class="id" type="var">re</span></span>, then <span class="inlinecode"><span class="id" type="var">s</span></span>
    can be split into three substrings <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>3</sub></span></span> in such a way
    that <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> can be repeated any number of times and the result, when
    combined with <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">s<sub>3</sub></span></span> will still match <span class="inlinecode"><span class="id" type="var">re</span></span>.  Since <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> is
    also guaranteed not to be the empty string, this gives us
    a (constructive!) way to generate strings matching <span class="inlinecode"><span class="id" type="var">re</span></span> that are
    as long as we like. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">pumping</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) <span class="id" type="var">s</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re</span> ≤ <span class="id" type="var">length</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">s<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> ++ <span class="id" type="var">s<sub>3</sub></span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> ≠ [] ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">m</span> <span class="id" type="var">s<sub>2</sub></span> ++ <span class="id" type="var">s<sub>3</sub></span> =~ <span class="id" type="var">re</span>.<br/>
</div>

<div class="doc">
To streamline the proof (which you are to fill in), the <span class="inlinecode"><span class="id" type="tactic">omega</span></span>
    tactic, which is enabled by the following <span class="inlinecode"><span class="id" type="keyword">Require</span></span>, is helpful in
    several places for automatically completing tedious low-level
    arguments involving equalities or inequalities over natural
    numbers.  We'll return to <span class="inlinecode"><span class="id" type="tactic">omega</span></span> in a later chapter, but feel
    free to experiment with it now if you like.  The first case of the
    induction gives an example of how it is used. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Import</span> <span class="id" type="var">Coq.omega.Omega</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">re</span> <span class="id" type="var">s</span> <span class="id" type="var">Hmatch</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hmatch</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [ | <span class="id" type="var">x</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span> | <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">re</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span> ].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Pumping</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab234"></a><h1 class="section">Case Study: Improving Reflection</h1>

<div class="paragraph"> </div>

 We've seen in the <a href="Logic.html"><span class="inlineref">Logic</span></a> chapter that we often need to
    relate boolean computations to statements in <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>.  But
    performing this conversion as we did it there can result in
    tedious proof scripts.  Consider the proof of the following
    theorem: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">filter_not_empty_In</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">n</span> =? <span class="id" type="var">x</span>) <span class="id" type="var">l</span> ≠ [] →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">m</span> <span class="id" type="var">l'</span> <span class="id" type="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;<span class="inlinecode"></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;m&nbsp;::&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? <span class="id" type="var">m</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;m&nbsp;=&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">eqb_eq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;m&nbsp;=&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHl'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
In the first branch after <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>, we explicitly apply
    the <span class="inlinecode"><span class="id" type="var">eqb_eq</span></span> lemma to the equation generated by
    destructing <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, to convert the assumption <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span>
    <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> into the assumption <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>; then we had to <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>
    using this assumption to complete the case. 
<div class="paragraph"> </div>

 We can streamline this by defining an inductive proposition that
    yields a better case-analysis principle for <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span>.
    Instead of generating an equation such as <span class="inlinecode">(<span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>,
    which is generally not directly useful, this principle gives us
    right away the assumption we really need: <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">reflect</span> (<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>) : <span class="id" type="var">bool</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ReflectT</span> (<span class="id" type="var">H</span> :   <span class="id" type="var">P</span>) : <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">true</span><br/>
| <span class="id" type="var">ReflectF</span> (<span class="id" type="var">H</span> : ¬<span class="id" type="var">P</span>) : <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">false</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="var">reflect</span></span> property takes two arguments: a proposition
    <span class="inlinecode"><span class="id" type="var">P</span></span> and a boolean <span class="inlinecode"><span class="id" type="var">b</span></span>.  Intuitively, it states that the property
    <span class="inlinecode"><span class="id" type="var">P</span></span> is <i>reflected</i> in (i.e., equivalent to) the boolean <span class="inlinecode"><span class="id" type="var">b</span></span>: that
    is, <span class="inlinecode"><span class="id" type="var">P</span></span> holds if and only if <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>.  To see this, notice
    that, by definition, the only way we can produce evidence for
    <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span> is by showing <span class="inlinecode"><span class="id" type="var">P</span></span> and then using the <span class="inlinecode"><span class="id" type="var">ReflectT</span></span>
    constructor.  If we invert this statement, this means that it
    should be possible to extract evidence for <span class="inlinecode"><span class="id" type="var">P</span></span> from a proof of
    <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span>.  Similarly, the only way to show <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span>
    <span class="inlinecode"><span class="id" type="var">false</span></span> is by combining evidence for <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span> with the <span class="inlinecode"><span class="id" type="var">ReflectF</span></span>
    constructor.

<div class="paragraph"> </div>

    It is easy to formalize this intuition and show that the
    statements <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">↔</span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> and <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> are indeed
    equivalent.  First, the left-to-right implication: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">iff_reflect</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">b</span>, (<span class="id" type="var">P</span> ↔ <span class="id" type="var">b</span> = <span class="id" type="var">true</span>) → <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">b</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">ReflectT</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">ReflectF</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="tactic">discriminate</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Now you prove the right-to-left implication: 
<div class="paragraph"> </div>

<a name="lab235"></a><h4 class="section">Exercise: 2 stars, standard, recommended (reflect_iff)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">reflect_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">b</span>, <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">b</span> = <span class="id" type="var">true</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The advantage of <span class="inlinecode"><span class="id" type="var">reflect</span></span> over the normal "if and only if"
    connective is that, by destructing a hypothesis or lemma of the
    form <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span>, we can perform case analysis on <span class="inlinecode"><span class="id" type="var">b</span></span> while at
    the same time generating appropriate hypothesis in the two
    branches (<span class="inlinecode"><span class="id" type="var">P</span></span> in the first subgoal and <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span> in the second). 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">eqbP</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">n</span> = <span class="id" type="var">m</span>) (<span class="id" type="var">n</span> =? <span class="id" type="var">m</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">eqb_eq</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
A smoother proof of <span class="inlinecode"><span class="id" type="var">filter_not_empty_In</span></span> now goes as follows.
    Notice how the calls to <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> and <span class="inlinecode"><span class="id" type="tactic">apply</span></span> are combined into a
    single call to <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
<div class="paragraph"> </div>

 (To see this clearly, look at the two proofs of
    <span class="inlinecode"><span class="id" type="var">filter_not_empty_In</span></span> with Coq and observe the differences in
    proof state at the beginning of the first case of the
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">filter_not_empty_In'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">n</span> =? <span class="id" type="var">x</span>) <span class="id" type="var">l</span> ≠ [] →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">m</span> <span class="id" type="var">l'</span> <span class="id" type="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;<span class="inlinecode"></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;m&nbsp;::&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqbP</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">H</span> | <span class="id" type="var">H</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;m&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;&lt;&gt;&nbsp;m&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHl'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab236"></a><h4 class="section">Exercise: 3 stars, standard, recommended (eqbP_practice)</h4>
 Use <span class="inlinecode"><span class="id" type="var">eqbP</span></span> as above to prove the following: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ 0<br/>
&nbsp;&nbsp;| <span class="id" type="var">m</span> :: <span class="id" type="var">l'</span> ⇒ (<span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? <span class="id" type="var">m</span> <span class="id" type="keyword">then</span> 1 <span class="id" type="keyword">else</span> 0) + <span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l'</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqbP_practice</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> = 0 → ~(<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 This small example shows how reflection gives us a small gain in
    convenience; in larger developments, using <span class="inlinecode"><span class="id" type="var">reflect</span></span> consistently
    can often lead to noticeably shorter and clearer proof scripts.
    We'll see many more examples in later chapters and in <i>Programming
    Language Foundations</i>.

<div class="paragraph"> </div>

    The use of the <span class="inlinecode"><span class="id" type="var">reflect</span></span> property has been popularized by
    <i>SSReflect</i>, a Coq library that has been used to formalize
    important results in mathematics, including as the 4-color theorem
    and the Feit-Thompson theorem.  The name SSReflect stands for
    <i>small-scale reflection</i>, i.e., the pervasive use of reflection to
    simplify small proof steps with boolean computations. 
</div>

<div class="doc">
<a name="lab237"></a><h1 class="section">Additional Exercises</h1>

<div class="paragraph"> </div>

<a name="lab238"></a><h4 class="section">Exercise: 3 stars, standard, recommended (nostutter_defn)</h4>
 Formulating inductive definitions of properties is an important
    skill you'll need in this course.  Try to solve this exercise
    without any help at all.

<div class="paragraph"> </div>

    We say that a list "stutters" if it repeats the same element
    consecutively.  (This is different from not containing duplicates:
    the sequence <span class="inlinecode">[1;4;1]</span> repeats the element <span class="inlinecode">1</span> but does not
    stutter.)  The property "<span class="inlinecode"><span class="id" type="var">nostutter</span></span> <span class="inlinecode"><span class="id" type="var">mylist</span></span>" means that <span class="inlinecode"><span class="id" type="var">mylist</span></span>
    does not stutter.  Formulate an inductive definition for
    <span class="inlinecode"><span class="id" type="var">nostutter</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">nostutter</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} : <span class="id" type="var">list</span> <span class="id" type="var">X</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
.<br/>
</div>

<div class="doc">
Make sure each of these tests succeeds, but feel free to change
    the suggested proof (in comments) if the given one doesn't work
    for you.  Your definition might be different from ours and still
    be correct, in which case the examples might need a different
    proof.  (You'll notice that the suggested proofs use a number of
    tactics we haven't talked about, to make them more robust to
    different possible ways of defining <span class="inlinecode"><span class="id" type="var">nostutter</span></span>.  You can probably
    just uncomment and use them as-is, but you can also prove each
    example with more basic tactics.)  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_1</span>: <span class="id" type="var">nostutter</span> [3;1;4;1;5;6].<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_neq;&nbsp;auto.<br/>
&nbsp;&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_2</span>:  <span class="id" type="var">nostutter</span> (@<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>).<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_neq;&nbsp;auto.<br/>
&nbsp;&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_3</span>:  <span class="id" type="var">nostutter</span> [5].<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_false;&nbsp;auto.&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_4</span>:      <span class="id" type="var">not</span> (<span class="id" type="var">nostutter</span> [3;1;1;4]).<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;intro.<br/>
&nbsp;&nbsp;repeat&nbsp;match&nbsp;goal&nbsp;with<br/>
&nbsp;&nbsp;&nbsp;&nbsp;h:&nbsp;nostutter&nbsp;_&nbsp;&#x22A2;&nbsp;_&nbsp;=&gt;&nbsp;inversion&nbsp;h;&nbsp;clear&nbsp;h;&nbsp;subst<br/>
&nbsp;&nbsp;end.<br/>
&nbsp;&nbsp;contradiction&nbsp;Hneq0;&nbsp;auto.&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_nostutter</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab239"></a><h4 class="section">Exercise: 4 stars, advanced (filter_challenge)</h4>
 Let's prove that our definition of <span class="inlinecode"><span class="id" type="var">filter</span></span> from the <span class="inlinecode"><span class="id" type="var">Poly</span></span>
    chapter matches an abstract specification.  Here is the
    specification, written out informally in English:

<div class="paragraph"> </div>

    A list <span class="inlinecode"><span class="id" type="var">l</span></span> is an "in-order merge" of <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> if it contains
    all the same elements as <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, in the same order as <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>
    and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, but possibly interleaved.  For example,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[1;4;6;2;3]
<div class="paragraph"> </div>

</div>
    is an in-order merge of

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[1;6;2]
<div class="paragraph"> </div>

</div>
    and

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[4;3].
<div class="paragraph"> </div>

</div>
    Now, suppose we have a set <span class="inlinecode"><span class="id" type="var">X</span></span>, a function <span class="inlinecode"><span class="id" type="var">test</span>:</span> <span class="inlinecode"><span class="id" type="var">X</span>→<span class="id" type="var">bool</span></span>, and a
    list <span class="inlinecode"><span class="id" type="var">l</span></span> of type <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>.  Suppose further that <span class="inlinecode"><span class="id" type="var">l</span></span> is an
    in-order merge of two lists, <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, such that every item
    in <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> satisfies <span class="inlinecode"><span class="id" type="var">test</span></span> and no item in <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> satisfies test.  Then
    <span class="inlinecode"><span class="id" type="var">filter</span></span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>.

<div class="paragraph"> </div>

    Translate this specification into a Coq theorem and prove
    it.  (You'll need to begin by defining what it means for one list
    to be a merge of two others.  Do this with an inductive relation,
    not a <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span>.)  
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_filter_challenge</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab240"></a><h4 class="section">Exercise: 5 stars, advanced, optional (filter_challenge_2)</h4>
 A different way to characterize the behavior of <span class="inlinecode"><span class="id" type="var">filter</span></span> goes like
    this: Among all subsequences of <span class="inlinecode"><span class="id" type="var">l</span></span> with the property that <span class="inlinecode"><span class="id" type="var">test</span></span>
    evaluates to <span class="inlinecode"><span class="id" type="var">true</span></span> on all their members, <span class="inlinecode"><span class="id" type="var">filter</span></span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> is the
    longest.  Formalize this claim and prove it. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab241"></a><h4 class="section">Exercise: 4 stars, standard, optional (palindromes)</h4>
 A palindrome is a sequence that reads the same backwards as
    forwards.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Define an inductive proposition <span class="inlinecode"><span class="id" type="var">pal</span></span> on <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> that
      captures what it means to be a palindrome. (Hint: You'll need
      three cases.  Your definition should be based on the structure
      of the list; just having a single constructor like

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">c</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>
<div class="paragraph"> </div>

</div>
      may seem obvious, but will not work very well.)

<div class="paragraph"> </div>


</li>
<li> Prove (<span class="inlinecode"><span class="id" type="var">pal_app_rev</span></span>) that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">pal</span>&nbsp;(<span class="id" type="var">l</span>&nbsp;++&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>).
<div class="paragraph"> </div>

</div>

</li>
<li> Prove (<span class="inlinecode"><span class="id" type="var">pal_rev</span></span> that)

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>

</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_pal_pal_app_rev_pal_rev</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab242"></a><h4 class="section">Exercise: 5 stars, standard, optional (palindrome_converse)</h4>
 Again, the converse direction is significantly more difficult, due
    to the lack of evidence.  Using your definition of <span class="inlinecode"><span class="id" type="var">pal</span></span> from the
    previous exercise, prove that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab243"></a><h4 class="section">Exercise: 4 stars, advanced, optional (NoDup)</h4>
 Recall the definition of the <span class="inlinecode"><span class="id" type="var">In</span></span> property from the <span class="inlinecode"><span class="id" type="var">Logic</span></span>
    chapter, which asserts that a value <span class="inlinecode"><span class="id" type="var">x</span></span> appears at least once in a
    list <span class="inlinecode"><span class="id" type="var">l</span></span>: 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Fixpoint&nbsp;In&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(x&nbsp;:&nbsp;A)&nbsp;(l&nbsp;:&nbsp;list&nbsp;A)&nbsp;:&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;match&nbsp;l&nbsp;with<br/>
&nbsp;&nbsp;&nbsp;|&nbsp;<span class="inlinecode"></span>&nbsp;=&gt;&nbsp;False<br/>
&nbsp;&nbsp;&nbsp;|&nbsp;x'&nbsp;::&nbsp;l'&nbsp;=&gt;&nbsp;x'&nbsp;=&nbsp;x&nbsp;\/&nbsp;In&nbsp;A&nbsp;x&nbsp;l'<br/>
&nbsp;&nbsp;&nbsp;end&nbsp;*)</span><br/>
</div>

<div class="doc">
Your first task is to use <span class="inlinecode"><span class="id" type="var">In</span></span> to define a proposition <span class="inlinecode"><span class="id" type="var">disjoint</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>
    <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>, which should be provable exactly when <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> are
    lists (with elements of type X) that have no elements in
    common. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<div class="doc">
Next, use <span class="inlinecode"><span class="id" type="var">In</span></span> to define an inductive proposition <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>
    <span class="inlinecode"><span class="id" type="var">l</span></span>, which should be provable exactly when <span class="inlinecode"><span class="id" type="var">l</span></span> is a list (with
    elements of type <span class="inlinecode"><span class="id" type="var">X</span></span>) where every member is different from every
    other.  For example, <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">[1;2;3;4]</span> and <span class="inlinecode"><span class="id" type="var">NoDup</span></span>
    <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">[]</span> should be provable, while <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">[1;2;1]</span> and
    <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">[<span class="id" type="var">true</span>;<span class="id" type="var">true</span>]</span> should not be.  
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<div class="doc">
Finally, state and prove one or more interesting theorems relating
    <span class="inlinecode"><span class="id" type="var">disjoint</span></span>, <span class="inlinecode"><span class="id" type="var">NoDup</span></span> and <span class="inlinecode">++</span> (list append).  
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_NoDup_disjoint_etc</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab244"></a><h4 class="section">Exercise: 4 stars, advanced, optional (pigeonhole_principle)</h4>
 The <i>pigeonhole principle</i> states a basic fact about counting: if
    we distribute more than <span class="inlinecode"><span class="id" type="var">n</span></span> items into <span class="inlinecode"><span class="id" type="var">n</span></span> pigeonholes, some
    pigeonhole must contain at least two items.  As often happens, this
    apparently trivial fact about numbers requires non-trivial
    machinery to prove, but we now have enough... 
<div class="paragraph"> </div>

 First prove an easy useful lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">in_split</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">x</span>:<span class="id" type="var">X</span>) (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span>, <span class="id" type="var">l</span> = <span class="id" type="var">l<sub>1</sub></span> ++ <span class="id" type="var">x</span> :: <span class="id" type="var">l<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Now define a property <span class="inlinecode"><span class="id" type="var">repeats</span></span> such that <span class="inlinecode"><span class="id" type="var">repeats</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> asserts
    that <span class="inlinecode"><span class="id" type="var">l</span></span> contains at least one repeated element (of type <span class="inlinecode"><span class="id" type="var">X</span></span>).  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">repeats</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} : <span class="id" type="var">list</span> <span class="id" type="var">X</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
.<br/>
</div>

<div class="doc">
Now, here's a way to formalize the pigeonhole principle.  Suppose
    list <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> represents a list of pigeonhole labels, and list <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>
    represents the labels assigned to a list of items.  If there are
    more items than labels, at least two items must have the same
    label &mdash; i.e., list <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> must contain repeats.

<div class="paragraph"> </div>

    This proof is much easier if you use the <span class="inlinecode"><span class="id" type="var">excluded_middle</span></span>
    hypothesis to show that <span class="inlinecode"><span class="id" type="var">In</span></span> is decidable, i.e., <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">l</span>,</span> <span class="inlinecode">(<span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>
    <span class="inlinecode"><span class="id" type="var">l</span>)</span> <span class="inlinecode">∨</span> <span class="inlinecode">¬</span> <span class="inlinecode">(<span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">l</span>)</span>.  However, it is also possible to make the proof
    go through <i>without</i> assuming that <span class="inlinecode"><span class="id" type="var">In</span></span> is decidable; if you
    manage to do this, you will not need the <span class="inlinecode"><span class="id" type="var">excluded_middle</span></span>
    hypothesis. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pigeonhole_principle</span>: <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">l<sub>1</sub></span>  <span class="id" type="var">l<sub>2</sub></span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">excluded_middle</span> →<br/>
&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l<sub>1</sub></span> → <span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">length</span> <span class="id" type="var">l<sub>2</sub></span> &lt; <span class="id" type="var">length</span> <span class="id" type="var">l<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">repeats</span> <span class="id" type="var">l<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">X</span> <span class="id" type="var">l<sub>1</sub></span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">x</span> <span class="id" type="var">l<sub>1</sub>'</span> <span class="id" type="var">IHl1'</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_check_repeats</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab245"></a><h2 class="section">Extended Exercise: A Verified Regular-Expression Matcher</h2>

<div class="paragraph"> </div>

 We have now defined a match relation over regular expressions and
    polymorphic lists. We can use such a definition to manually prove that
    a given regex matches a given string, but it does not give us a
    program that we can run to determine a match autmatically.

<div class="paragraph"> </div>

    It would be reasonable to hope that we can translate the definitions
    of the inductive rules for constructing evidence of the match relation
    into cases of a recursive function reflects the relation by recursing
    on a given regex. However, it does not seem straightforward to define
    such a function in which the given regex is a recursion variable
    recognized by Coq. As a result, Coq will not accept that the function
    always terminates.

<div class="paragraph"> </div>

    Heavily-optimized regex matchers match a regex by translating a given
    regex into a state machine and determining if the state machine
    accepts a given string. However, regex matching can also be
    implemented using an algorithm that operates purely on strings and
    regexes without defining and maintaining additional datatypes, such as
    state machines. We'll implemement such an algorithm, and verify that
    its value reflects the match relation. 
<div class="paragraph"> </div>

 We will implement a regex matcher that matches strings represented
    as lists of ASCII characters: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Strings.Ascii</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">string</span> := <span class="id" type="var">list</span> <span class="id" type="var">ascii</span>.<br/>
</div>

<div class="doc">
The Coq standard library contains a distinct inductive definition
    of strings of ASCII characters. However, we will use the above
    definition of strings as lists as ASCII characters in order to apply
    the existing definition of the match relation.

<div class="paragraph"> </div>

    We could also define a regex matcher over polymorphic lists, not lists
    of ASCII characters specifically. The matching algorithm that we will
    implement needs to be able to test equality of elements in a given
    list, and thus needs to be given an equality-testing
    function. Generalizing the definitions, theorems, and proofs that we
    define for such a setting is a bit tedious, but workable. 
<div class="paragraph"> </div>

 The proof of correctness of the regex matcher will combine
    properties of the regex-matching function with properties of the
    <span class="inlinecode"><span class="id" type="keyword">match</span></span> relation that do not depend on the matching function. We'll go
    ahead and prove the latter class of properties now. Most of them have
    straightforward proofs, which have been given to you, although there
    are a few key lemmas that are left for you to prove. 
</div>

<div class="doc">
Each provable <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">True</span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">provable_equiv_true</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>), <span class="id" type="var">P</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">True</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="var">constructor</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Each <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> whose negation is provable is equivalent to <span class="inlinecode"><span class="id" type="var">False</span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">not_equiv_false</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>), ¬<span class="id" type="var">P</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">False</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptySet</span></span> matches no string. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">null_matches_none</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>), (<span class="id" type="var">s</span> =~ <span class="id" type="var">EmptySet</span>) ↔ <span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> only matches the empty string. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_matches_eps</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>), <span class="id" type="var">s</span> =~ <span class="id" type="var">EmptyStr</span> ↔ <span class="id" type="var">s</span> = [ ].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">MEmpty</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> matches no non-empty string. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_nomatch_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, (<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">EmptyStr</span>) ↔ <span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> matches no string that starts with a non-<span class="inlinecode"><span class="id" type="var">a</span></span> character. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">char_nomatch_char</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> <span class="id" type="var">b</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, <span class="id" type="var">b</span> ≠ <span class="id" type="var">a</span> → (<span class="id" type="var">b</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Char</span> <span class="id" type="var">a</span> ↔ <span class="id" type="var">False</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
If <span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> matches a non-empty string, then the string's tail is empty. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">char_eps_suffix</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Char</span> <span class="id" type="var">a</span> ↔ <span class="id" type="var">s</span> = [ ].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> matches string <span class="inlinecode"><span class="id" type="var">s</span></span> iff <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>, where <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span>
    matches <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> and <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">app_exists</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">App</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span> ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s<sub>2</sub></span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">split</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>3</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> [ <span class="id" type="var">s<sub>0</sub></span> [ <span class="id" type="var">s<sub>1</sub></span> [ <span class="id" type="var">Happ</span> [ <span class="id" type="var">Hmat0</span> <span class="id" type="var">Hmat1</span> ] ] ] ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Happ</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> <span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">_</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">_</span> <span class="id" type="var">Hmat0</span> <span class="id" type="var">Hmat1</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab246"></a><h4 class="section">Exercise: 3 stars, standard, optional (app_ne)</h4>
 <span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> iff <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> matches the empty string
    and <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> or <span class="inlinecode"><span class="id" type="var">s</span>=<span class="id" type="var">s<sub>0</sub></span>++<span class="id" type="var">s<sub>1</sub></span></span>, where <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s<sub>0</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span>
    and <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>.

<div class="paragraph"> </div>

    Even though this is a property of purely the match relation, it is a
    critical observation behind the design of our regex matcher. So (1)
    take time to understand it, (2) prove it, and (3) look for how you'll
    use it later. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">app_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ (<span class="id" type="var">App</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>) ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;([ ] =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span>) ∨<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="var">s</span></span> matches <span class="inlinecode"><span class="id" type="var">Union</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> iff <span class="inlinecode"><span class="id" type="var">s</span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> or <span class="inlinecode"><span class="id" type="var">s</span></span> matches <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">union_disj</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span> ↔ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>0</sub></span> ∨ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> [ <span class="id" type="var">H</span> | <span class="id" type="var">H</span> ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">MUnionL</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">MUnionR</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab247"></a><h4 class="section">Exercise: 3 stars, standard, optional (star_ne)</h4>
 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> matches <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> iff <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>, where <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s<sub>0</sub></span></span> matches
    <span class="inlinecode"><span class="id" type="var">re</span></span> and <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> matches <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>. Like <span class="inlinecode"><span class="id" type="var">app_ne</span></span>, this observation is
    critical, so understand it, prove it, and keep it in mind.

<div class="paragraph"> </div>

    Hint: you'll need to perform induction. There are quite a few
    reasonable candidates for <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>'s to prove by induction. The only one
    that will work is splitting the <span class="inlinecode"><span class="id" type="var">iff</span></span> into two implications and
    proving one by induction on the evidence for <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>. The
    other implication can be proved without induction.

<div class="paragraph"> </div>

    In order to prove the right property by induction, you'll need to
    rephrase <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> to be a <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> over general variables,
    using the <span class="inlinecode"><span class="id" type="var">remember</span></span> tactic.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span> <span class="id" type="var">re</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re</span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The definition of our regex matcher will include two fixpoint
    functions. The first function, given regex <span class="inlinecode"><span class="id" type="var">re</span></span>, will evaluate to a
    value that reflects whether <span class="inlinecode"><span class="id" type="var">re</span></span> matches the empty string. The
    function will satisfy the following property: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">refl_matches_eps</span> <span class="id" type="var">m</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>, <span class="id" type="var">reflect</span> ([ ] =~ <span class="id" type="var">re</span>) (<span class="id" type="var">m</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab248"></a><h4 class="section">Exercise: 2 stars, standard, optional (match_eps)</h4>
 Complete the definition of <span class="inlinecode"><span class="id" type="var">match_eps</span></span> so that it tests if a given
    regex matches the empty string: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">match_eps</span> (<span class="id" type="var">re</span>: @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab249"></a><h4 class="section">Exercise: 3 stars, standard, optional (match_eps_refl)</h4>
 Now, prove that <span class="inlinecode"><span class="id" type="var">match_eps</span></span> indeed tests if a given regex matches
    the empty string.  (Hint: You'll want to use the reflection lemmas
    <span class="inlinecode"><span class="id" type="var">ReflectT</span></span> and <span class="inlinecode"><span class="id" type="var">ReflectF</span></span>.) 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">match_eps_refl</span> : <span class="id" type="var">refl_matches_eps</span> <span class="id" type="var">match_eps</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 We'll define other functions that use <span class="inlinecode"><span class="id" type="var">match_eps</span></span>. However, the
    only property of <span class="inlinecode"><span class="id" type="var">match_eps</span></span> that you'll need to use in all proofs
    over these functions is <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span>. 
</div>

<div class="doc">
The key operation that will be performed by our regex matcher will
    be to iteratively construct a sequence of regex derivatives. For each
    character <span class="inlinecode"><span class="id" type="var">a</span></span> and regex <span class="inlinecode"><span class="id" type="var">re</span></span>, the derivative of <span class="inlinecode"><span class="id" type="var">re</span></span> on <span class="inlinecode"><span class="id" type="var">a</span></span> is a regex
    that matches all suffixes of strings matched by <span class="inlinecode"><span class="id" type="var">re</span></span> that start with
    <span class="inlinecode"><span class="id" type="var">a</span></span>. I.e., <span class="inlinecode"><span class="id" type="var">re'</span></span> is a derivative of <span class="inlinecode"><span class="id" type="var">re</span></span> on <span class="inlinecode"><span class="id" type="var">a</span></span> if they satisfy the
    following relation: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">is_der</span> <span class="id" type="var">re</span> (<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">re'</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">s</span>, <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> ↔ <span class="id" type="var">s</span> =~ <span class="id" type="var">re'</span>.<br/>
</div>

<div class="doc">
A function <span class="inlinecode"><span class="id" type="var">d</span></span> derives strings if, given character <span class="inlinecode"><span class="id" type="var">a</span></span> and regex
    <span class="inlinecode"><span class="id" type="var">re</span></span>, it evaluates to the derivative of <span class="inlinecode"><span class="id" type="var">re</span></span> on <span class="inlinecode"><span class="id" type="var">a</span></span>. I.e., <span class="inlinecode"><span class="id" type="var">d</span></span>
    satisfies the following property: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">derives</span> <span class="id" type="var">d</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">re</span>, <span class="id" type="var">is_der</span> <span class="id" type="var">re</span> <span class="id" type="var">a</span> (<span class="id" type="var">d</span> <span class="id" type="var">a</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab250"></a><h4 class="section">Exercise: 3 stars, standard, optional (derive)</h4>
 Define <span class="inlinecode"><span class="id" type="var">derive</span></span> so that it derives strings. One natural
    implementation uses <span class="inlinecode"><span class="id" type="var">match_eps</span></span> in some cases to determine if key
    regex's match the empty string. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">derive</span> (<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">derive</span></span> function should pass the following tests. Each test
    establishes an equality between an expression that will be
    evaluated by our regex matcher and the final value that must be
    returned by the regex matcher. Each test is annotated with the
    match fact that it reflects. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">c</span> := <span class="id" type="var">ascii_of_nat</span> 99.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">d</span> := <span class="id" type="var">ascii_of_nat</span> 100.<br/>
</div>

<div class="doc">
"c" =~ EmptySet: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der0</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">EmptySet</span>)) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Char c: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der1</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>)) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Char d: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der2</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>)) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ App (Char c) EmptyStr: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der3</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>) <span class="id" type="var">EmptyStr</span>)) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ App EmptyStr (Char c): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der4</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> <span class="id" type="var">EmptyStr</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Star c: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der5</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Star</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"cd" =~ App (Char c) (Char d): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der6</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">d</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>) (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>)))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"cd" =~ App (Char d) (Char c): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der7</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">d</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>) (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>)))) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
<a name="lab251"></a><h4 class="section">Exercise: 4 stars, standard, optional (derive_corr)</h4>
 Prove that <span class="inlinecode"><span class="id" type="var">derive</span></span> in fact always derives strings.

<div class="paragraph"> </div>

    Hint: one proof performs induction on <span class="inlinecode"><span class="id" type="var">re</span></span>, although you'll need
    to carefully choose the property that you prove by induction by
    generalizing the appropriate terms.

<div class="paragraph"> </div>

    Hint: if your definition of <span class="inlinecode"><span class="id" type="var">derive</span></span> applies <span class="inlinecode"><span class="id" type="var">match_eps</span></span> to a
    particular regex <span class="inlinecode"><span class="id" type="var">re</span></span>, then a natural proof will apply
    <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span> to <span class="inlinecode"><span class="id" type="var">re</span></span> and destruct the result to generate cases
    with assumptions that the <span class="inlinecode"><span class="id" type="var">re</span></span> does or does not match the empty
    string.

<div class="paragraph"> </div>

    Hint: You can save quite a bit of work by using lemmas proved
    above. In particular, to prove many cases of the induction, you
    can rewrite a <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> over a complicated regex (e.g., <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Union</span></span>
    <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>) to a Boolean combination of <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>'s over simple
    regex's (e.g., <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>) using lemmas given above
    that are logical equivalences. You can then reason about these
    <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>'s naturally using <span class="inlinecode"><span class="id" type="tactic">intro</span></span> and <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">derive_corr</span> : <span class="id" type="var">derives</span> <span class="id" type="var">derive</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 We'll define the regex matcher using <span class="inlinecode"><span class="id" type="var">derive</span></span>. However, the only
    property of <span class="inlinecode"><span class="id" type="var">derive</span></span> that you'll need to use in all proofs of
    properties of the matcher is <span class="inlinecode"><span class="id" type="var">derive_corr</span></span>. 
</div>

<div class="doc">
A function <span class="inlinecode"><span class="id" type="var">m</span></span> matches regexes if, given string <span class="inlinecode"><span class="id" type="var">s</span></span> and regex <span class="inlinecode"><span class="id" type="var">re</span></span>,
    it evaluates to a value that reflects whether <span class="inlinecode"><span class="id" type="var">s</span></span> is matched by
    <span class="inlinecode"><span class="id" type="var">re</span></span>. I.e., <span class="inlinecode"><span class="id" type="var">m</span></span> holds the following property: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">matches_regex</span> <span class="id" type="var">m</span> : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) (<span class="id" type="var">m</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab252"></a><h4 class="section">Exercise: 2 stars, standard, optional (regex_match)</h4>
 Complete the definition of <span class="inlinecode"><span class="id" type="var">regex_match</span></span> so that it matches
    regexes. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">regex_match</span> (<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab253"></a><h4 class="section">Exercise: 3 stars, standard, optional (regex_refl)</h4>
 Finally, prove that <span class="inlinecode"><span class="id" type="var">regex_match</span></span> in fact matches regexes.

<div class="paragraph"> </div>

    Hint: if your definition of <span class="inlinecode"><span class="id" type="var">regex_match</span></span> applies <span class="inlinecode"><span class="id" type="var">match_eps</span></span> to
    regex <span class="inlinecode"><span class="id" type="var">re</span></span>, then a natural proof applies <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span> to <span class="inlinecode"><span class="id" type="var">re</span></span>
    and destructs the result to generate cases in which you may assume
    that <span class="inlinecode"><span class="id" type="var">re</span></span> does or does not match the empty string.

<div class="paragraph"> </div>

    Hint: if your definition of <span class="inlinecode"><span class="id" type="var">regex_match</span></span> applies <span class="inlinecode"><span class="id" type="var">derive</span></span> to
    character <span class="inlinecode"><span class="id" type="var">x</span></span> and regex <span class="inlinecode"><span class="id" type="var">re</span></span>, then a natural proof applies
    <span class="inlinecode"><span class="id" type="var">derive_corr</span></span> to <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">re</span></span> to prove that <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re</span></span> given
    <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">derive</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>, and vice versa. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">regex_refl</span> : <span class="id" type="var">matches_regex</span> <span class="id" type="var">regex_match</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Wed&nbsp;Jan&nbsp;9&nbsp;12:02:45&nbsp;EST&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>